Give the Seq model named array and length fields#161
Merged
Conversation
This was referenced Jul 1, 2026
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 84a3441e3b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
coord-e
force-pushed
the
claude/seq-named-fields
branch
2 times, most recently
from
8b876de to
c720ea2
Compare
Replace the positional `Seq<T>(Array<Int, T>, Int)` tuple struct with a
named-field struct `Seq { array, length }`, and refer to the fields by
name throughout the extern specs and tests instead of `.0`/`.1`.
Struct literals are now supported in specification formulas: an
`ExprKind::Struct` is lowered to a tuple with fields placed at their
declaration position, mirroring how struct field access already resolves
named fields to positions.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi
coord-e
force-pushed
the
claude/seq-named-fields
branch
from
c720ea2 to
ecd5d85
Compare
Contributor
There was a problem hiding this comment.
Pull request overview
This PR is the first step in a larger refactor to replace the positional Seq<T>(Array<Int, T>, Int) tuple model with a named-field Seq { array, length }, updating extern specs and UI tests accordingly and adding support for struct literals in specification formulas.
Changes:
- Convert the
Seqmodel definition from a tuple struct to a named-field struct (array,length). - Update extern specs and UI tests to use
.array/.lengthinstead of.0/.1(with explicit*where needed). - Lower
ExprKind::Structspecification formulas into tuple terms in declaration order.
Reviewed changes
Copilot reviewed 18 out of 18 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| tests/ui/pass/slice_methods.rs | Update slice spec assertions to use array/length named fields (explicit deref). |
| tests/ui/pass/slice_methods_mut.rs | Update mut slice spec assertions to use array/length. |
| tests/ui/pass/slice_last_mut.rs | Update last-element spec assertions to use array/length. |
| tests/ui/pass/slice_index.rs | Update indexing spec assertions to use array/length. |
| tests/ui/pass/slice_index_mut.rs | Update mut indexing spec assertions to use array/length. |
| tests/ui/pass/slice_first_mut.rs | Update first-element spec assertions to use array/length. |
| tests/ui/pass/seq_specs_vec_build.rs | Update Vec build spec to compare against result.array/result.length. |
| tests/ui/pass/loop_invariant_fn_param_at_entry.rs | Update invariant/spec to use .length field access. |
| tests/ui/fail/slice_methods.rs | Update failing slice spec to use array/length named fields. |
| tests/ui/fail/slice_methods_mut.rs | Update failing mut slice spec to use array/length. |
| tests/ui/fail/slice_last_mut.rs | Update failing last-element spec to use array/length. |
| tests/ui/fail/slice_index.rs | Update failing indexing spec to use array/length. |
| tests/ui/fail/slice_index_mut.rs | Update failing mut indexing spec to use array/length. |
| tests/ui/fail/slice_first_mut.rs | Update failing first-element spec to use array/length. |
| tests/ui/fail/seq_specs_vec_build.rs | Update failing Vec build spec to use array/length. |
| tests/ui/fail/loop_invariant_fn_param_at_entry.rs | Update failing invariant/spec to use .length field access. |
| std.rs | Redefine Seq with named fields and update Vec/slice extern specs to refer to them. |
| src/analyze/annot_fn.rs | Add lowering for struct literals in spec formulas (ExprKind::Struct). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This is PR 1 of 4 in a restructuring of #153 into reviewable steps.
Replace the positional
Seq<T>(Array<Int, T>, Int)tuple struct with a named-field structSeq { array, length }, and refer to the fields by name (.array/.length) throughout the extern specs and tests instead of.0/.1.Details
ExprKind::Structis lowered to a tuple with fields placed at their declaration position, mirroring how struct field access already resolves named fields to positions..0/.1access only worked through references incidentally (via unboxing), so dereferences through&/&mutreceivers are now written explicitly in the annotations, e.g.(*slice).length.Validation
cargo build,cargo fmt --all -- --check,cargo clippy -- -D warningscargo test— all Spacer-backed UI tests and the reconstruction unit tests pass. (The PCSat-backed tests were not run in this environment as they require the CoAR Docker image.)Stack
concat_int_arraytakes sequence tuplessplit_first/split_last(_mut)🤖 Generated with Claude Code
https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi